Inference at * 1 1 
Iof proof for Lemma dep ax choice:



1. A : Type
2. B : AType
3. Q : x:AB(x)Type
4. x:Ay:B(x)  Q(x,y)
  f:x:AB(x). (x:A. Q(x,f(x))) 

latex

 by ((((((With z.(g(z)).1 (D 0)) 
CollapseTHENM (D 0))) 
CollapseTHENM (Reduce 0))) 

CoCollapseTHENA ((Auto_aux (first_nat 1:n) ((first_nat 1:n),(first_nat 3:n)) (first_tok :t
C) inil_term))) 

latex

C1: 

C1: 5. x : A
C1:   Q(x,(g(x)).1)
C.

Definitions	x. t(x), t  T, x:A. B(x), x:A. B(x), x(s1,s2), x(s)
Lemmas	pi1 wf